    DEF X(X:nat):nat == X
    DEF Y(X:nat, Y:nat):nat == X(Y)
    DEF MAIN:bool == true
